(declare-fun s0 () (_ FloatingPoint 11 53))
(declare-fun s1 () (_ FloatingPoint 11 53))
(declare-fun s2 () (_ FloatingPoint 11 53))
(assert (let ((s3 (fp.isZero s1))) (let ((s4 (fp.isNegative s1))) (let ((s5 (and s3 s4))) (let ((s6 (fp.isZero s2))) (let ((s7 (fp.isPositive s2))) (let ((s8 (and s6 s7))) (let ((s9 (fp.min s1 s2))) (let ((s10 (= s0 s9))) (and s5 s8 s10))))))))))
(check-sat)
(declare-fun s0 () (_ FloatingPoint 11 53))
(declare-fun s1 () (_ FloatingPoint 11 53))
(declare-fun s2 () (_ FloatingPoint 11 53))
(assert (let ((s3 (fp.isZero s2))) (let ((s4 (fp.isNegative s2))) (let ((s5 (and s3 s4))) (let ((s6 (fp.isZero s1))) (let ((s7 (fp.isPositive s1))) (let ((s8 (and s6 s7))) (let ((s9 (fp.max s1 s2))) (let ((s10 (= s0 s9))) (and s5 s8 s10))))))))))
(check-sat)
